\section{Alternation Elimination}

We implement two different constructions. The 2-Way Miyano-Hayashi construction is described in the paper and translates a loop-free locally 1-way 2ABA (lfl1-2ABA) into a 1NBA. For LTL inputs, the intermediate lfl1-2ABA is very weak. For these kind of automata we use the 2-Way Gastin-Oddoux construction.

\subsection{2-Way Miyano-Hayashi Construction}
Let $\autA = (Q, \delta, \qI, F)$ be a loop-free locally 1-way 2ABA. Define $R := \setx{r_q}{q \in Q}$ and $S := \setx{s_q}{q \in Q \setminus F}$, and for a set $S$ we define $S':=\setx{s'}{s \in S}$ as the primed version of the given set. We define a language-equivalent 1NBA $\autB = (O, \eta, \oI, E)$\footnote{A 1NBA with a set of initial states accepts a word if there is an accepting run on the word that starts with one of the initial states.} in the following way.

\begin{itemize}
	\item $O := 2^{R \cup S}$
	
	\item $\oI := \setx{M \in O}{M \models r_{\qI} \land C \land \bigwedge_{q \in Q \setminus F} \neg s_q}$, where%
	%
	\footnote{Note that $\delta(q)$ is a \emph{positive} boolean combination of states.}$^,$%
	\footnote{An alternative way to describe the initial states would be as follows. First, for every $q \in Q$, we substitute every $(q', -1)$ in $\delta(q)$ by $(Yq', 0)$. Then, we define the set of initial states as the sets that contain $\qI$ and that do not contain states of the form $(Yq,0)$.}
	%
		\[
			C := \bigwedge_{p \in Q} r_p \to \delta(p)
				[\false / (q, -1), 
				\true / (q, \opZ),
				r_q / (q, 0),
				\true / (q, 1)]
		\]%
		
	\item $E := \setx{M \in O}{M \models \bigwedge_{q \in Q \setminus F} \neg s_q}$
	
	\item $\eta = \setx{M \in O \cup O'}{M \models C_1 \land C_2 \land C_3 \land C_4}$, where
		\begin{align*}
			&C_1 := \bigwedge_{p \in Q} r_p \to \delta(p)
				[\true / (q, -1), 
				\true / (q, \opZ), 
				r_q / (q, 0), 
				r'_q / (q, 1)], \\
			%
			&C_2 := \bigwedge_{p \in Q} r'_p \to \delta(p)
				[r_q / (q, -1), 
				r_q / (q, \opZ), 
				r'_q / (q, 0), 
				\true / (q, 1),
				a' / a], \\
			%
			&C_3 := (\bigwedge_{q \in Q \setminus F} \neg s_q) \to 
				\bigwedge_{q \in Q \setminus F} (r'_q \leftrightarrow s'_q), \\
			%
			&C_4 := (\bigvee_{q \in Q \setminus F} s_q) \to C_{41} \land C_{42}, \\
			&\qquad C_{41} := \bigwedge_{p \in Q \setminus F} (s_p \to \delta(p)
				[\true / (q, -1), 
				\true / (q, \opZ), 
				f(q) / (q, 0), 
				f(q)' / (q, 1)], \\			
			&\qquad C_{42} := \bigwedge_{p \in Q \setminus F} (s'_p \to \delta(p)
				[f(q) / (q, -1), 
				f(q) / (q, \opZ), 
				f(q)' / (q, 0), 
				\true / (q, 1),
				a' / a],
		\end{align*}
		where $f:Q \to Q \cup Q'$, $f(q) := r_q$ if $q \in F$, and $s_q$, otherwise.
\end{itemize}


\subsection{2-Way Gastin-Oddoux Construction}
\newcommand{\nxt}{\mathop{next}}

Let $\autA = (Q, \delta, \qI, F)$ be a \emph{very weak} loop-free locally 1-way 2ABA. We define $R := \setx{r_q}{q \in Q}$, $S := \setx{s_q}{q \in Q \setminus F} \cup \set{s_!}$, and $\sigma: |S| \to S$ be an injective function. For a set $T$, we write $T':=\setx{t'}{t \in T}$ as the primed version of the set $T$. We define the language-equivalent 1NBA $\autB = (O, \eta, \oI, E)$ in the following way.

\begin{itemize}
	\item $O := \setx{T \cup \set{s}}{(T, s) \in 2^R \times S}$
	
	\item $\oI := \setx{M \in O}{M \models r_{\qI} \land C \land s_!}$, where%
		\[
			C := \bigwedge_{p \in Q} r_p \to \delta(p)
				[\false / (q, -1), 
				\true / (q, \opZ),
				r_q / (q, 0),
				\true / (q, 1)]
		\]%
		
	\item $E := \setx{M \in O}{M \models s_!}$
	
	\item $\eta = \setx{M \in O \cup O'}{M \models C_1 \land C_2 \land C_3 \land C_4}$, where
		\begin{align*}
			&C_1 := \bigwedge_{p \in Q} r_p \to \delta(p)
				[\true / (q, -1), 
				\true / (q, \opZ), 
				r_q / (q, 0), 
				r'_q / (q, 1)], \\
			%
			&C_2 := \bigwedge_{p \in Q} r'_p \to \delta(p)
				[r_q / (q, -1), 
				r_q / (q, \opZ), 
				r'_q / (q, 0), 
				\true / (q, 1),
				a' / a], \\
			%
			&C_3 := \bigwedge_{0 \le i \le |S|} (\sigma(i) \to 
				(\Phi_{\sigma(i)} \to \sigma(j)') \land 
				(\neg\Phi_{\sigma(i)} \to \sigma(i)')), \\
			&\qquad j := i+1 \mod |S| \\
			&\qquad \Phi_p := 
				\begin{cases}
					\true & \text{if $p = s_!$} \\
					r_p \to
					\delta(p)
						[\true / (q, -1), 
						\true / (q, \opZ), 
						r_q / (q, 0), 
						r'_q / (q, 1),
						\false / r'_p] & \text{otherwise}
				\end{cases}
			%
		\end{align*}
\end{itemize}
